$\forall$$A$, $B$:Type, ${\it opa}$:($A$$\rightarrow$$A$$\rightarrow$$A$), ${\it opb}$:($B$$\rightarrow$$B$$\rightarrow$$B$), $f$:($A$$\rightarrow$$B$). FunThru2op($A$;$B$;${\it opa}$;${\it opb}$;$f$) $\in$ $\mathbb{P}$